T:Type, E:(TT).
EquivRel(T;x,y.E(x,y))  (x, y:T. Dec(E(x,y)))  (u, v:(x,y:T//E(x,y)). Dec(u = v)) 

latex

Up	quot 1, quot 1
Definitions	x,y. t(x;y), t  T, x(s1,s2), P  Q, , x:A. B(x), P & Q, P  Q, P  Q, x:A. B(x), x f y, True, T, Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), EquivRel(T;x,y.E(x;y)), SqStable(P), S  T
Lemmas	equiv rel wf, decidable wf, quotient wf, dec iff ex bvfun, bool wf, iff imp equal bool, assert wf, iff functionality wrt iff, iff wf, sq stable equal, decidable assert, sq stable from decidable, sq stable iff, quotient qinc, squash wf